module Z where

-- No "let/where" in the function definitions 

-- Zeno doesn't use anything from the Prelude
-- you have to define it all from scratch
import Prelude ()


-- Monomorphic datatypes only

data Nat = Zero | Suc Nat
data List = Nil | Cons Nat List
data Bool = True | False


-- Boolean functions

and :: Bool -> Bool -> Bool
and True True = True
and _ _ = False

not :: Bool -> Bool
not True = False
not False = True


-- Natural number functions

add :: Nat -> Nat -> Nat
add Zero y = y
add (Suc x) y = Suc (add x y)

add2 Zero y = y
add2 (Suc x) y = add x (Suc y)

mul :: Nat -> Nat -> Nat
mul Zero _ = Zero
mul (Suc x) y = add y (mul x y)

eq :: Nat -> Nat -> Bool
eq Zero Zero = True
eq Zero _ = False
eq (Suc _) Zero = False
eq (Suc x) (Suc y) = eq x y

leq :: Nat -> Nat -> Bool
leq Zero _ = True
leq (Suc x) Zero = False
leq (Suc x) (Suc y) = leq x y

less :: Nat -> Nat -> Bool
less _ Zero = False
less Zero _ = True
less (Suc x) (Suc y) = less x y

min :: Nat -> Nat -> Nat
min Zero y = Zero
min (Suc x) Zero = Zero
min (Suc x) (Suc y) = Suc (min x y)

max :: Nat -> Nat -> Nat
max Zero y = y
max x Zero = x
max (Suc x) (Suc y) = Suc (max x y)

min2 :: Nat -> Nat -> Nat
min2 x y =
  case leq x y of
    True -> x
    False -> y   
    
max2 :: Nat -> Nat -> Nat
max2 x y =
  case leq x y of
    True -> y
    False -> x

minus :: Nat -> Nat -> Nat
minus Zero _ = Zero
minus x Zero = x
minus (Suc x) (Suc y) = minus x y

alwaysTrue :: Nat -> Bool
alwaysTrue _ = True

alwaysFalse :: Nat -> Bool
alwaysFalse _ = False

-- Monomorphism is a pain in the ass
comp :: (Nat -> Nat) -> (Nat -> Bool) -> Nat -> Bool
comp f p n = p (f n)


-- List functions

concat :: List -> List -> List
concat Nil ys = ys
concat (Cons x xs) ys = Cons x (concat xs ys)

rev :: List -> List
rev Nil = Nil
rev (Cons x xs) = concat (rev xs) (Cons x Nil)

listEq :: List -> List -> Bool
listEq Nil Nil = True
listEq (Cons _ _) Nil = False
listEq Nil (Cons _ _) = False
listEq (Cons x xs) (Cons y ys) = 
  (x `eq` y) `and` (xs `listEq` ys)

null :: List -> Bool
null Nil = True
null _ = False

minimum :: List -> Nat
minimum Nil = Zero
minimum (Cons x Nil) = x
minimum (Cons x xs) =
  case leq x (minimum xs) of
    True -> x
    False -> minimum xs
    
elem :: Nat -> List -> Bool
elem _ Nil = False
elem n (Cons x xs) = 
  case n `eq` x of
    True -> True
    False -> elem n xs

qrev :: List -> List -> List
qrev Nil ys = ys
qrev (Cons x xs) ys = qrev xs (Cons x ys) 
    
drop :: Nat -> List -> List
drop Zero xs = xs
drop _ Nil = Nil
drop (Suc x) (Cons _ xs) = drop x xs

take :: Nat -> List -> List
take Zero _ = Nil
take _ Nil = Nil
take (Suc x) (Cons y ys) = Cons y (take x ys) 

len :: List -> Nat
len Nil = Zero
len (Cons _ xs) = Suc (len xs)

count :: Nat -> List -> Nat
count x Nil = Zero
count x (Cons y ys) =
  case x `eq` y of
    True -> Suc (count x ys)
    False -> count x ys

butlast :: List -> List
butlast Nil = Nil
butlast (Cons x Nil) = Nil
butlast (Cons x xs) = Cons x (butlast xs)

last :: List -> Nat
last Nil = Zero
last (Cons x Nil) = x
last (Cons x xs) = last xs

map :: (Nat -> Nat) -> List -> List
map f Nil = Nil
map f (Cons x xs) = Cons (f x) (map f xs)

takeWhile :: (Nat -> Bool) -> List -> List
takeWhile _ Nil = Nil
takeWhile p (Cons x xs) = 
  case p x of
    True -> Cons x (takeWhile p xs)
    False -> Nil
    
dropWhile :: (Nat -> Bool) -> List -> List
dropWhile _ Nil = Nil
dropWhile p (Cons x xs) =
  case p x of
    True -> dropWhile p xs
    False -> Cons x xs
    
filter :: (Nat -> Bool) -> List -> List
filter _ Nil = Nil
filter p (Cons x xs) = 
  case p x of
    True -> Cons x (filter p xs)
    False -> filter p xs
    
delete :: Nat -> List -> List
delete _ Nil = Nil
delete a (Cons x xs) = 
  case a `eq` x of
    True -> delete a xs
    False -> Cons a (delete a xs)
    
sorted :: List -> Bool
sorted Nil = True
sorted (Cons x Nil) = True
sorted (Cons x (Cons y ys)) = 
  case x `leq` y of
    False -> False
    True -> sorted (Cons y ys)
    
insert :: Nat -> List -> List
insert x Nil = Cons x Nil
insert x (Cons y ys) =
  case x `leq` y of
    True -> Cons x (Cons y ys)
    False -> Cons y (insert x ys)   
    
insertsort :: List -> List
insertsort Nil = Nil
insertsort (Cons x xs) = insert x (insertsort xs)

-- Properties that Zeno can successfully prove
{- Zeno

addzero (x : Nat) 
  add x Zero = x.

revrev (xs : List)
  rev (rev xs) = xs.

eqsym (x : Nat) (y : Nat)
  eq x y = True :- eq y x = True.

add2 (x : Nat) (y : Nat)
  add x y = add2 x y.
  
qrev (xs : List) (ys : List)
  concat (rev xs) ys = qrev xs ys.

maplen (f : Nat -> Nat) (xs : List)
  len xs = len (map f xs).
  
maprev (f : Nat -> Nat) (xs : List)
  rev (map f xs) = map f (rev xs).
  
takeall (xs : List)
  takeWhile alwaysTrue xs = xs.
  
dropnone (xs : List)
  dropWhile alwaysFalse xs = xs.
  
mapfilter (f : Nat -> Nat) (P : Nat -> Bool) (xs : List)
  filter P (map f xs) = map f (filter (comp f P) xs).

sucminus (x : Nat) (y : Nat) (z : Nat)
  minus (minus (Suc x) y) (Suc z) = minus (minus x y) z.

insertlen (x : Nat) (xs : List)
  len (insert x xs) = Suc (len xs).

lesslast (n : Nat) (xs : List)
  last (drop n xs) = last xs :- less n (len xs) = True.

lastconcat (xs : List) (ys : List)
  last (concat xs ys) = last xs :- ys = Nil.

minmin2 (x : Nat) (y : Nat)
  min2 x y = min2 y x.

testwhile (P : Nat -> Bool) (xs : List)
  concat (takeWhile P xs) (dropWhile P xs) = xs. 
  
eqsym (x : Nat) (y : Nat)
  eq x y = True :- eq y x = True.

lastcons (x : Nat) (xs : List)
  last (Cons x xs) = x :- xs = Nil.
  
countadd (n : Nat) (xs : List) (ys : List)
  add (count n xs) (count n ys) = count n (concat xs ys).

countrev (x : Nat) (xs : List)
  count x xs = count x (rev xs).
  
countreveq (x : Nat) (xs : List)
  eq (count x xs) (count x (rev xs)) = True.
  
countsort (x : Nat) (xs : List)
  count x xs = count x (insertsort xs).

concatnil (x : Nat) (xs : List)
  concat (rev xs) (Cons x Nil) = Nil.

minusadd2 (i : Nat) (j : Nat) (k : Nat)
  minus (minus i j) k = minus i (add j k).
  
takeconcat (n : Nat) (xs : List) (ys: List)
  take n (concat xs ys) = concat (take n xs) (take (minus n (len xs)) ys).
  
takedrop (n : Nat) (xs : List) (ys: List)
  concat (take n xs) (drop n xs) = xs.
  
dropadd (n : Nat) (m : Nat) (xs : List) 
  drop n (drop m xs) = drop (add n m) xs.
  
takedropadd (n : Nat) (m : Nat) (xs : List)
  take n (drop m xs) = drop m (take (add n m) xs).
  
blconcat (x : Nat) (xs : List)
  butlast (concat xs (Cons x Nil)) = xs.
 
minmin (x : Nat) (y : Nat)
  min x y = min y x.
 
maxmax (x : Nat) (y : Nat)
  max x y = max y x.

onezero (x : Bool)
  Suc Zero = Zero :- x = True, x = False.

eqtrn (x : Nat) (y : Nat) (z : Nat)
  eq x z = True :- eq x y = True, eq y z = True.
  
filterrev (P : Nat -> Bool) (xs : List)
  filter P (rev xs) = rev (filter P xs).
  
nullnil (xs : List)
  xs = Nil :- null xs = True.

minusadd (x : Nat) (y : Nat)
  minus (add x y) y = x.
  
dropconcat (n : Nat) (xs : List) (ys: List)
  drop n (concat xs ys) = concat (drop n xs) (drop (minus n (len xs)) ys).
  
leqadd (x : Nat) (y : Nat)
  leq x (add y x) = True.

bltake (xs : List)
  butlast xs = take (minus (len xs) (Suc Zero)) xs.
  
minminmin (x : Nat) (y : Nat) (z : Nat)
  min x (min y z) = min (min x y) z.
  
muladd (x : Nat) (y : Nat) (z : Nat)
  mul x (add y z) = add (mul x y) (mul x z).
  
droptake (n : Nat) (m : Nat) (xs : List) 
  drop n (take m xs) = take (minus m n) (drop n xs).

elemmin (n : Nat) (x : Nat) (xs : List)
  leq (minimum xs) n :- elem n xs.

sortinginsert (x : Nat) (xs : List)
  sorted (insert x xs) :- sorted xs.

verifysort (xs : List)
  sorted (insertsort xs).

lenfilter (P : Nat -> Bool) (xs : List)
  leq (len (filter P xs)) (len xs).

lendelete (x : Nat) (xs : List)
  leq (len (delete x xs)) (len xs).

neqelem (x : Nat) (y : Nat) (xs : List)
  elem x (insert y xs) = elem x xs :- not (eq x y).

-}

-- Properties that Zeno fails to prove
{- Zeno

revreveq (xs : List)
  listEq (rev (rev xs)) xs = True.
  
revtake (i : Nat) (xs : List)
  rev (take i xs) = drop (minus (len xs) i) (rev xs).

revdrop (i : Nat) (xs : List)
  rev (drop i xs) = take (minus (len xs) i) (rev xs).
  
takelenrev (n : Nat) (x : Nat) (xs : List)
  take (len xs) (rev xs) = take (len xs) (concat (rev xs) (Cons x xs)).

-}

